Nuprl Lemma : mon_itop_unroll_lo 13,42

g:IMonoid, ij:.
(i < j (E:({i..j}|g|). ( i  k < jE(k)) = (E(i) * ( i+1  k < jE(k)))  |g|) 
latex


Upgroups 1
Definitions of Statement lb  i < ubE(i)
Definitions lb  i < ubE(i)
Lemmasitop unroll lo

origin